the_w:World, i:Id, a:Action(i). isnull(a)  kind(a)  Knd 

latex

Definitions	true, false, False, True, x. t(x), World, Action(i), isnull(a), kind(a), w.TA, w.M, P  Q, 1of(t), outr(x), Knd, A, b, isl(x), , Action(dec), w-action-dec(TA;M;i), x:A. B(x), t  T, Id
Lemmas	Id wf, w-action-dec wf, action wf, assert wf, not wf, world wf, Knd wf, pi1 wf, bfalse wf, btrue wf